$\forall$$T$:Type. 
\\[0ex]subtype\_rel($T$; $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$, $L$:($T$ List). sorted(cons($x$; $L$)) $\Leftarrow\!\Rightarrow$ (sorted($L$) $\wedge$ l\_all($L$; $T$; $z$.($x$ $\leq$ $z$))))